COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\\M0BDR40\M1NGR30\.
C00005 ENDMK
C⊗;
\\M0BDR40;\M1NGR30;\.
\F0\CARTIFICIAL INTELLIGENCE LABORATORY
\CDEPARTMENT OF COMPUTER SCIENCE
\CSTANFORD UNIVERSITY
\CSTANFORD, CALIFORNIA 94305
\F1


						November 21, 1973

Miss Jean M. Hodgson
Senior Administrative Officer
Faculty of Science Office
University of Edinburgh
West Mains Road
Edinburgh, Scotland EH9 3JY

Dear Miss Hodgson:

\J	Thank you for your request for my opinion of the prospective
appointment of Robin Milner as Reader.  I have no hesitation in
recommending him without qualification.

	Robin came to Stanford for what was originally intended as a
one year appointment at the recommendation of Zohar Manna who was 
impressed by his theoretical work in mathematical theory of computation.
While here, he not only continued his theoretical work but also developed
the first really practical system for checking proofs of the correctness
of computer programs.  This system LCF has been used for checking 
proofs of the correctness of more substantial programs than has any
other program, and it is still being used and developed several years
later.  The development of this system required an ability to combine
mathematical sophistication with practicality in a way that is quite
rare.  Now that the ice has been broken, it is not difficult to get
mathematical logicians to use it and extend it, but without Robin
Milner, we might still be without such a system.

	His continued theoretical work also shows a clear understanding
of what the important problems and real issues are in making proving
programs correct a practical matter.

	We made every effort to keep him at Stanford, but his desire
to return to Britain was too strong for us.\.


						Sincerely yours,


						John McCarthy
						Professor of Computer Science
						Director, Artificial Intelligence Laboratory